306 X EXISTENCE THEOREMS Now the bilinear mapping (X, 7)~ğ X° Y of jSf(E) x^(E) into is continuously differentiable (8.1.4); denote by R(t) the continuous linear mapping U-ğA(t) ° Uof JS?(E) into itself. From (5.7.5) it follows at once that \\R(t)~R(t')\\*:\\A(t)-A(t')\\ hence, if K =R, t^R(t) is regulated ift-+A(t) is regulated. On the other hand, if / -> ^((f) is difFerentiable, so is / -> ^(0, and its derivative at the point / (identified (Section 8.4) to an element of <£(E)) is the mapping U-+ A'(t) ° U ((8.1.3) and (8.2.1)); hence if t~+ A'(t) is continuous, so is f-ğ R'(t}. We can therefore conclude that if K = C and if / -> A(t) is analytic in I, so is t -> J?(/) (9.10.1). In any case, we may apply (10.6.4) to the equation (10.8.4.1); let V(t) be the solution of that equation equal to 7E for t = s. We have, for any /el ((8.1. 3) and (8.2.1)) *o) = V(f) • *0 = -4(0 and furthermore, for t = s, V(s) - x0 = 7E • x0 = x0 ; it therefore follows from (10.6.4) applied to (10.8.3) that C(t, s)-x0= V(t) - x0 for any JCQ e E, hence C(t, s) = V(t) for t e I. This proves that C(t, s) e jSf(E) and that * -> C(/, j) is the solution of (10.8.4.1) which is equal to /E for t = s. Finally, the function /-ğ C(t, r) - x0 is the solution of (10.8.3) equal to C(s9 r) - XQ for t = s; hence, by definition C(t, r)-x0~ C(t, s) • (C(s9 r) • x0) = (C(t, s) ° C(s9 r)) • x0 for any x0 e E, which proves the first relation (1 0.8.4.2) ; as C(t9 1) = 7E , that relation yields C(t, s) ° C(s, t) = JE. This shows that C(s9 1) is a bfjective linear mapping of E, whose inverse mapping is C(t9 s) (hence also belongs to JS?(E)). With this we reach the end of the proof of (1 0.8.4). The operator C(t9 s) is called the resolvent of (10.8.3) (or of (10.6.2)) in I. (10.8.5) The mapping (s, t) -> C(s91) oflxl into jSf(E) is continuous. We may indeed write C(s91) = C(s910) ° (C(r, /0))~"\ and the result then follows from (10.8.4), (5.7.5), and (8.3.2). The knowledge of C(s91) enables one to give the explicit solution of (10.6.2) taking the value JCQ for t = t0: (10.8.6) The function ii(0 = C(t, t0) • x0 + \(C(t, s) • b(s)) ds Jto or ,y = /, y = u(t9 tQ , x0) = ;c, which ends the proof. nique solution v of (10.4.1)